done. I'm not very experienced at squashing commits. If that's a thing you care about I could either figure out how to do that, or delete this PR and push a new one ...

Squashing is the best. Nomatter how many individual ones you pile up we end up with one.

(I became a fan of amending commits though when 'n + 1' is just a subtle refinement of 'n' and to then force-push (if in branch / fork))

(So when I squash in a minute or two you will have three lines for the three commits in the expanded commit message. Someone sufficiently type-a to not want three could simply do a standard git squashing to reduce the three to two or one. It lets you. Squash-merge added that to the web ui.)